
\subsection{Undecidability of Eventual Adaptation in \evold{3}}
Here we prove that \LG %negative reachability  
is undecidable for \evold{3} processes.
We obtain this result by means of a non-faithful encoding of \mmss similar to the one presented before.

In that encoding, Definition \ref{def:minskyconfs}, process deletion was used
to restore the initial state inside the adaptable processes representing
the registers. In the absence of process deletion, 
we use a more involved technique based on the
possibility of moving processes to a different context:
processes to be removed are guarded by an update
prefix $\update{c_j}{\component{c_j}{\bullet}}$
that simply tests for the presence of a parallel adaptable process at $c_{j}$;
when a process must be deleted, it is 
``collected'' inside $c_{j}$, thus
disallowing the possibility to execute such an update prefix.

\begin{table}[t] 
\linefigure\\
\quad\\

\centering  
{ 
\begin{tabular}{l}   
$\controll ~= ~!a.(\outC{f} \parallel \outC{b} \parallel  \outC{a}) \parallel \outC{a}.a.(\outC{p_1} \parallel e) \parallel \
!h.(g.\outC{f} \parallel \outC{h})$
  \\
$\mathrm{\textsc{Register}}~r_j $ \\ 
\ \ \(  
\encp{r_j = 0 }{\mmn{3}}= \component{r_j}{Reg_j \parallel \component{c_j}{\nil}} 
\) \\
\ \ $\mbox{with~} Reg_j = !inc_j.\update{c_j}{\component{c_j}{\bullet}}.\outC{ack}.u_j.\update{c_j}{\component{c_j}{\bullet}}.\outC{ack}$
\\
\(
\begin{array}{lll}
\multicolumn{3}{l}{\! \! \mathrm{\textsc{Instructions}}~(i:I_i)}\\  
\encp{(i: \mathtt{INC}(r_j))}{\mmn{3}}&  = &  !p_i.f.(\outC{g} \parallel
b.\outC{inc_j}.
ack.\outC{p_{i+1}}) \\
\encp{(i: \mathtt{DECJ}(r_j,s))}{\mmn{3}}&  = & !p_i.f.\big(\outC{g} \parallel(\outC{u_j}.%(\outC{w}+
ack.(\outC{b} \parallel %w . 
\outC{p_{i+1}})  + \\%)
&& \qquad \qquad \qquad \update{c_j}{\bullet}.\update{r_j}{\component{r_j}{Reg_j \parallel
\component{c_j}{\bullet}}}.\outC{p_s})\big) \\
\encp{(i: \mathtt{HALT})}{\mmn{3}}&  = & !p_i.%w.
\outC{h}.h.\update{c_0}{\bullet}.\update{r_0}{\component{r_0}{Reg_0 \parallel \component{c_0}{\bullet}}}. \\
&& \qquad \qquad \qquad \update{c_1}{\bullet}.\update{r_1}{\component{r_1}{Reg_1 \parallel
\component{c_1}{\bullet}}}.\outC{p_1}
\end{array}   
\)
\end{tabular}
}  
\caption{Encoding of \mmss into \evold{3}.}  
\label{t:encod-evold3d}  
 \linefigure
\end{table}



The encoding is as in 
Definition~\ref{def:minskyconfs}, with registers
and instructions encoded as  in Table~\ref{t:encod-evold3d}:

\begin{definition}\label{def:minskyconfsevol3d}
 Let $N$ be a \mm, with registers $r_0$, $r_1 $ and instructions
$(1:I_1) \ldots (n:I_n)$. 
Given the \controll process and the encodings in 
Table~\ref{t:encod-evold3d}, the encoding of $N$ in \evold{3} (written $\encp{N}{\mmn{3}}$)
is defined as
$
\encp{r_0 = 0}{\mmn{3}} \parallel \encp{r_1 = 0}{\mmn{3}} \parallel \prod^{n}_{i=1} \encp{(i:I_i)}{\mmn{3}}  
 \parallel \controll$.
\end{definition}


A register $r_j$ that stores number $m$ is encoded as an adaptable process at $r_j$ that
contains $m$ copies of the unit process $u_j.\update{c_j}{\component{c_j}{\bullet}}.\outC{ack}$. 
It also contains
process $Reg_j$, which creates further copies of the unit
process when an increment instruction is invoked, as well as 
the collector $c_j$, which  is used to store the
processes to be removed.

An increment instruction adds an occurrence of $u_j.\update{c_j}{\component{c_j}{\bullet}}.\outC{ack}$. Note that %it could occur that 
an output 
$\outC{inc}$ could synchronize with the corresponding input inside a collected process. This immediately leads to deadlock as the containment induced by $c_j$ prevents further interactions.
The encoding of a decrement-and-jump instruction is implemented as a
choice, following the idea discussed for the static case.
If the process guesses that the register is zero then, before jumping to the given instruction, it proceeds at disabling its current content: 
this is done by 
(i) removing the boundary of the collector $c_{j}$ 
%thus merging the active processes inside $r_{j}$ and $c_{j}$, 
leaving its content at the top-level, 
and (ii) updating the register placing its previous state in the collector.
A decrement simply consumes one occurrence of $u_j.\update{c_j}{\component{c_j}{\bullet}}.\outC{ack}$. 
Note that as before %it could occur that 
the output 
$\outC{u_j}$ could synchronize with the corresponding input inside a collected process. 
Again, this immediately leads to deadlock.
The encoding of $\mathtt{HALT}$ exploits the same mechanism of
collecting processes to simulate the reset of the registers.


This encoding has the same properties of the one discussed
for the static case. In fact, in an infinite simulation the collected
processes are never involved, otherwise the computation would block.



\begin{lemma}\label{th:corrE3}
 Let $N$ be a \mm. $N$ terminates iff $\encp{N}{\mms} \barbw{e}$.
\end{lemma}
\begin{proof}
See \ref{app:e31}.
\end{proof}

Lemma \ref{th:corrE3} allows to conclude 
that $\LG$ is undecidable for processes in \evold{3}. The proof of the following theorem proceeds  as the proofs of Theorems \ref{th.ev1} and \ref {th:ev2}.

\begin{theorem}
\LG is undecidable in \evold{3}.
\end{theorem}
%\begin{proof}[Sketch]
%Let $N$ be a \mma and and consider its encoding $\encp{N}{\mms}$. We have $\BC_{\encp{N}{\mms}}^{\emptyset}=\{\encp{N}{\mms}\}$.
%%consider the very simple cluster $C = \bullet$. 
%Undecidability of \LG  %$C[\encp{N}{\mms}]\negbarbk{\overline{e}}$ 
%follows from undecidability of the termination problem for Minsky machines
%and Lemma \ref{th:corrE3}. \qed
%%Then $C[\encp{N}{\mms}]\barbw{\overline{e}}$ immediately follows from Theorem \ref{th:corrE2}.\ref{th:corrE3}. \qed
%\end{proof}


We can conclude that process deletion is not necessary for proving 
the undecidability of $\LG$ in \evold{3}. Nevertheless, in the encoding
in Table~\ref{t:encod-evold3d} we need to use the possibility to 
remove and create adaptable processes (namely, the collectors $c_{j}$
are removed and then reproduced when the registers must be reset).
One could therefore wonder whether $\LG$ is still undecidable if we 
remove from \evold{3}  the possibility to remove 
processes. Next we  show that this is not the case.



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%\newpage

\subsection{Decidability of Eventual Adaptation in \evols{3}}\label{sec:evol3}

We prove the decidability of \LG in \evols{3} %eventual adaptation
by resorting to Petri nets. Namely, we reduce the 
eventual adaptation problem for \evols{3}
to the 
infinite visit problem (cf. Definition \ref{d:infvisit}).
%place boundedness problem for Petri nets.
%
%
%an infinite-state
%concurrent computational 
%model for which several  problems are  
%decidable~(see, e.g., \cite{EN94}). 



%\todo{Elaborate further on the difficulty of the reduction. This is related to the abstraction assumed (that is claimed to be not problematic).}



Before formally defining the encoding of \evols{3} processes into Petri nets, we give some intuitions.
The idea is to use the markings of the Petri net
to represent the active sequential subprocesses and the available
adaptable processes. Transitions are used to model the execution of
actions. More precisely, each active sequential subprocess is represented
by one token. Two tokens corresponding to two sequential subprocesses
able to execute complementary actions can fire a transition,
whose effect is to produce tokens representing the two continuations. 
As for update actions,
they are represented by transitions that consume (at least) two 
tokens: one token corresponding to the process executing the update and another token
representing the adaptable process target of the update operations. 
In order to ensure that update actions take place between processes which are in parallel, 
%It is necessary to check that the 
%process is not in the target adaptable process, as 
%a process can update only adaptable processes in parallel with it.
%To this aim, we need to 
we keep track of the adaptable processes in which
a process is included: we do so by decorating its place with a list of outer adaptable processes.
Intuitively, this list represents the ``address'' of a single adaptable process within the nested structure 
of adaptable processes.
%\todo{We should use another letter for the addresses: $\alpha$ is commonly used for barbs}

We now present some auxiliary notations required by the definition.
Let $P$ be a process of $\evols{3}$ and 
$M=\{P_{1},\ldots,P_{n}\}$ be a set of processes of $\evols{3}$.
%\todo{Perhaps this is the ``abstraction'' that could be further explained:}
It is not restrictive to assume that all the update actions on a given adaptable process  can be executed:
even if the static semantics decrees that update actions should satisfy conditions on the nesting structure of adaptable processes,
Theorem~\ref{stdynequiv} ensures the existence of an \evold{} process with the same behavior for which such conditions are always true.
%In the light of Theorem~\ref{stdynequiv} it is not restrictive
%to assume that all the
%update actions on $a$ can be executed on every 
%adaptable process at $a$ (even if under the static semantics
%an update action can be executed only if the update does not
%modify the  nesting structure of adaptable processes).
Let $\pseq(P,M)$ be the set of sequential subprocesses in 
$P,P_{1},\ldots,P_{n}$ and let $\ambpaths(P,M)$ be the 
set of location names nestings, i.e. strings composed
of names of nested locations, starting from the outermost
adaptable process, occurring in one of the processes $P,P_{1},\ldots,P_{n}$.
We use $\sigma, \theta$ to range over strings in $\ambpaths(P,M)$, 
and write $\sigma a$ for the string obtained from concatenating $\sigma$ and $a$.

\begin{definition}\label{d:pn}
Let $P$ and $M=\{P_{1},\ldots,P_{n}\}$ be \evols{3} processes. Its
associated Petri net is defined as the triple
$$\pnr{P}{M}=(\places{P,M},\transit{P,M},\initMark{P})$$
%$$(\places{P,M},\transit{P,M},\initMark{P})$$
where
\begin{itemize}
\item $\places{P,M}=  \{\coppia{P}{\sigma}\ |\  P \in 
\pseq(P,M), \, \sigma \in \ambpaths(P,M)\} \cup \ambpaths(P,M) \cup
\{start, go\}$,  with $start$ and $go$ being two distinguished auxiliary places. 


%\item The set of transitions $\transit{P,M}$ is defined as the instantiations to places in $\places{P,M}$ of the transitions schemata in Table~\ref{tab:pn}.

%\todo{This is not very clear, I would write:
\item $\transit{P,M}$ contains all the instances of the transition schemata reported in Table~\ref{tab:pn} over the set of places $\places{P,M}$.

%The set T rans contains all the instances of the transition schemata reported in Table 1

\item $\initMark{P} = \decc{\varepsilon}{P} \uplus \{start\}$,
with $\decc{\sigma}{P}$
defined inductively as follows: %\todo{Why not $\initMark{P,M}$?}
\begin{align*}
\decc{\sigma}{\component{a}{P}} & =  \decc{\sigma a}{P} \uplus \{\sigma a\} \\
\decc{\sigma}{P \parallel P'} & =  \decc{\sigma}{P} \uplus \decc{\sigma}{P'}\\ 
\decc{\sigma}{P} & =  \{\coppia{P}{\sigma}\} \quad \mbox{otherwise} 
\end{align*}
where 
$\varepsilon$
corresponds to the empty string and
$\uplus$ denotes multiset union.
\end{itemize}

\end{definition}
%The set of places  of the corresponding Petri net, denoted $\places{P,M}$,
% is defined
%as $ \{\coppia{P}{\alpha}\ |\  P \in 
%\pseq(P,M), \alpha \in \ambpaths(P,M)\} \uplus
%\{start, go\}$, 
%where $start$
%%, $check$, 
%and
%$go$ %, and $stop$
%are distinct auxiliary places.

We now describe the Petri net computation by giving intuitions on the transitions presented in Table~\ref{tab:pn}.
The initial marking includes one token in the place $start$
plus the tokens corresponding to the active 
sequential subprocesses of $P$. 
%Formally, these are the places 
%$\decc{\varepsilon}(P)$ (with $\varepsilon$
%corresponding to the empty string) where $\decc{\alpha}(P)$
%is defined inductively as follows:
%\begin{eqnarray*}
%\decc{\alpha}(\component{a}{P}) & = & \decc{\alpha a}(P) \uplus \{\alpha a\} \\
%\decc{\alpha}(P \parallel P') & = & \decc{\alpha}(P) \uplus \decc{\alpha}(P')\\ 
%\decc{\alpha}(P) & = & \{\coppia{P}{\alpha}\} \quad \mbox{otherwise} 
%\end{eqnarray*}
%where $\uplus$ denotes multiset union.
%The initial marking is
%$\initMark{P} = \decc{\varepsilon}(P) \uplus \{start\}$. 
%
The token in $start$ allows to generate an arbitrary amount 
of copies of the processes $P_{1},\ldots,P_{n} \in M$ (Transition (1)). This is simply achieved
by considering $n$ transitions, such that the $i$-th transition
tests for the presence of the token in $start$ and then produces the 
sequential subprocesses of $P_{i}$.
Nondeterministically, the token is moved from $start$ to $go$ (Transition (2)).
At this point, the simulation of the evolution of the generated
configuration is started. As described above, synchronizations 
between complementary actions are modeled by transitions that consume
the tokens corresponding to the two synchronizing processes
and then produce the sequential subprocesses in the continuations.
Transitions (3)--(5) cover the different cases in which an input/output synchronization
can arise (namely, interaction between two guarded processes, between a replicated processes and a guarded process, and
between two replicated processes), while
Transitions (6)--(9) cover the cases 
in which a synchronization corresponds to an update action.
In the latter kind of transitions, we need to check the availability
of a target adaptable process, but this adaptable process should not enclose
the updating process (as in, e.g., $\component{a}{\update{a}{U} \parallel P}$).
More precisely, 
suppose there is a process $Q$ executing an update action on name $a$, and let $\sigma$ 
be the string of the names of the adaptable processes enclosing $Q$.
The availability of a target adaptable process can be checked by verifying 
the presence of  a token in a place $\theta a$ which is not a prefix of $\sigma$
(see Transitions (6) and (8)).
If $\theta a$ is a prefix of $\sigma$, then the adaptable process at $\theta a$ could enclose $Q$.
In such a  case, it is sufficient to check that the place $\theta a$ contains at least two tokens, 
thus indicating the
existence of a different adaptable process with the same path but that does not enclose $Q$
(see Transitions (7) and (9)).


%Formally, we define the set of transitions $\transit{P,M}$ as
%the instantiations to places in $\places{P,M}$ of the transitions
%schemata in Table~\ref{tab:pn}.
%So we can formally define the Petri net for the given
%process $P$ and the set of processes $M$ as the
%triple $(\places{P,M},\transit{P,M},\initMark{P,M})$.

\begin{table}[!ht]
\linefigure

\[
\begin{array}{ll}
(1) & \{start\} \derriv \{start\} \uplus \decc{\varepsilon}{P_{i}}\ \ \ \ \ \text{with}\ P_{i} \in M 
\\
\\
(2)& \{start\} \derriv \{go\}
\\
\\
(3)&\{go,  \coppia{\sum_{i \in I} \pi_i.A_i}{\sigma},
           \coppia{\sum_{j \in J} \rho_j.B_j}{\theta}\}
          \derriv
          \{go\}\uplus \decc{\sigma}{A_{l}}
\uplus \decc{\theta}{B_{m}}
          \\
          &
          \mbox{if $\pi_{l}=a$ and $\rho_{m}=\overline{a}$
          (for $l \in I$, $m \in J$)}
          \\
          \\
          
(4)&\{go, \coppia{!\pi.A}{\sigma},
           \coppia{ \sum_{j \in J} \rho_j.B_j}{\theta}\}
          \derriv \\
& \qquad \qquad \quad
          \{go, \coppia{!\pi.A}{\sigma}\} \uplus
\decc{\sigma}{A} \uplus \decc{\theta}{B_{m}}
          \\
          &
          \mbox{if $\pi=a$ (resp. $\overline{a}$) and $\rho_{m}=\overline{a}$ (resp. $a$)
          (for $m \in J$)}
          \\
          \\
          
(5)& \{go, \coppia{!\pi.A}{\sigma},
          \coppia{!\rho.B}{\theta}\}
          \derriv\\
& \qquad \qquad \quad
          \{go, \coppia{!\pi.A}{\sigma}, 
\coppia{!\rho.B}{\theta} \} \uplus
\decc{\sigma}{A}  \uplus \decc{\theta}{B_{m}}
          \\
          &
          \mbox{if $\pi=a$ (resp. $\overline{a}$) and $\rho=\overline{a}$ (resp. $a$)
          }
          \\
          \\

(6)& \{go, \coppia{\sum_{i \in I} \pi_i.A_i}{\sigma},\theta a\}
 \derriv\\
& \qquad \qquad \quad
 \{go\} \uplus \decc{\sigma}{A_{l}} \uplus 
 \decc{\theta}{A} 
 \uplus \decc{\theta a}{U}
 \uplus \{\theta a\}
           \\
           &
           \mbox{if $\theta a$ is not a prefix of $\sigma$,
           $\pi_{l}=
           \update{a}{\component{a}{U} \parallel A}$
           (for $l \in I$)}    
\\
\\
(7)& \{go, \coppia{\sum_{i \in I} \pi_i.A_i}{\sigma},\theta a,\theta a\}
 \derriv \\
& \qquad \qquad \quad
 \{go\} \uplus \decc{\sigma}{A_{l}} \uplus 
 \decc{\theta}{A}
 \uplus \decc{\theta a}{U}
 \uplus \{\theta a,\theta a\}
           \\
           &
           \mbox{if $\theta a$ is a prefix of $\sigma$,
           $\pi_{l}=
           \update{a}{\component{a}{U}\parallel A}$
           (for $l \in I$)}   

\\
\\
(8)& \{go, \coppia{!\pi.A'}{\sigma},\theta a\}
 \derriv \\
& \qquad \qquad \quad
 \{go, \coppia{!\pi.A'}{\sigma}\} \uplus
 \decc{\sigma}{A'} \uplus 
 \decc{\theta}{A} 
 \uplus \decc{\theta a}{U}
 \uplus \{\theta a\}
           \\
           &
           \mbox{if $\theta a$ is not a prefix of $\sigma$,
           $\pi=
           \update{a}{\component{a}{U} \parallel A}$
           }    
\\
\\
(9)& \{go, \coppia{!\pi.A'}{\sigma},\theta a,\theta a\}
 \derriv \\
 & \qquad \qquad  \quad \{go,  \coppia{!\pi.A'}{\sigma}\} \uplus \decc{\sigma}{A'} \uplus 
 \decc{\theta}{A} 
 \uplus \decc{\theta a}{U}
 \uplus \{\theta a,\theta a\}
           \\
           &
           \mbox{if $\theta a$ is a prefix of $\sigma$,
           $\pi=
           \update{a}{\component{a}{U} \parallel A}$
           }                          
\end{array}
\]
\caption{Transition schemata for the Petri net representation of $\evols{3}$ processes in Definition \ref{d:pn}.}\label{tab:pn}
 \linefigure
\end{table}


We now state the correspondence between %$\evols{3}$
processes
and their associated Petri net.

\begin{lemma}\label{lem:initpetri}
 Let $P$ be a process of $\evols{3}$,
and $M$ be the set $\{P_{1},\cdots,P_{n}\}$ and $(\places{P,$ $M}, \transit{P,M}, \initMark{P})$
 be their associated Petri net,  as in Definition \ref{d:pn}. Then, given a marking $m$, we have
$\initMark{P} \rightarrow^* \{start\} \uplus m \rightarrow   \{go\} \uplus m$ iff  $m = \decc{\varepsilon}{R}$, for some $R \in \BC_P^M$.
\end{lemma}
\begin{proof}
 Follows by construction of the Petri net.
\end{proof}




\begin{lemma}\label{l:pn}
 Let $P$ and $(\places{P,\emptyset}, \transit{P,\emptyset}, \initMark{P})$
 be an \evols{3} process and its associated Petri net,  as in Definition \ref{d:pn}.
 Then we have:
$$P \pired P' \textrm{ iff } \decc{\varepsilon}{P} \uplus \{go\} \rightarrow  \decc{\varepsilon}{P'} \uplus \{go\}.$$
\end{lemma}
\begin{proof}

See  \ref{app:e32}, page \pageref{app:e32}.
\end{proof}


The decidability of \LG for $\evols{3}$ follows
from the decidability of the existence of a suffix
of an infinite computation composed of markings with at least
one token in some given places. 

\begin{theorem}\label{th:pnev3}
Let $P$ be a process of $\evols{3}$,
and let $M$ be the set $\{P_{1},\cdots,P_{n}\}$ of 
processes of $\evols{3}$.
Consider $S = \CStrs(P) \cup \CStrs(P_{1}) \cup \cdots \cup \CStrs(P_{n})$,
and let $P' = \dyn{P}$ and $M' = \{\dyn{P_{1}},\cdots,\dyn{P_{n}}\}$.
Let $\alpha$ be a barb.
We have that $P$ and $M$ satisfies \LG for the
barb $\alpha$ iff the 
Petri net $$(\places{P',M'}, \transit{P',M'}, \initMark{P'})$$
has an infinite computation with a suffix composed
of markings with one token in $go$ and 
with at least one token in one of the places 
$\coppia{\sum_{i \in I} \pi_i.A_i}{\theta}$, with 
$\pi_{l}=\alpha$ for some $l\in I$, or
$\coppia{!\alpha.A}{\theta}$. 
\end{theorem}

\begin{proof}
Suppose that $P$ and $M$ satisfies \LG for the
barb $\alpha$ then there exists a process $R \in \BC_P^M$ such that $R \barb{\alpha}^{\omega}$.
Following from Lemma \ref{lem:initpetri} there exists an initial computation of the Petri net that reaches the marking $\decc{\varepsilon}{R} \uplus \{ go \}$. Then following from Lemma \ref{l:pn} there exists an  infinite computation with a suffix composed
of markings with at least one token in one of the places 
$\coppia{\sum_{i \in I} \pi_i.A_i}{\theta}$, with 
$\pi_{l}=\alpha$ for some $l\in I$, or
$\coppia{!\alpha.A}{\theta}$. Notice that in all of these
markings, the place $go$ contains one token.

Similarly if there exists   an  infinite computation with a suffix composed
of markings with one token in $go$ and at least one token in one of the places 
$\coppia{\sum_{i \in I} \pi_i.A_i}{\theta}$, with 
$\pi_{l}=\alpha$ for some $l\in I$, or
$\coppia{!\alpha.A}{\theta}$ then for Lemma \ref{lem:initpetri} and Lemma \ref{l:pn}  we know that there exists a process $R \in \BC_P^M$ such that $R \barb{\alpha}^{\omega}$.
\end{proof}

%To check that a given barb  $\alpha$
%can be exposed infinitely often by contiguous states,
%we simply check the existence of an infinite
%computation in the Petri net 
%having a suffix that traverses markings 
%containing at least one token in places
%representing a 
%sequential processes able to execute the action $\alpha$.
The check %in a Petri net
of the existence of an infinite computation
with a suffix composed of markings with one token in $go$ and
with at least one
token in some given places 
corresponds to the infinite visit problem (Definition~\ref{d:infvisit}).
%can be done using the
%coverability tree~\cite{KarpM69,Finkel93}: it is sufficient to verify
%the existence of a path in the coverability tree traversing the nodes
%$m_{1},\ldots,m_{k}$, where $m_{k}$ is a leaf of the tree 
%greater than $m_{1}$ (i.e. $m_{1}(p) \leq m_{k}(p)$ for every place $p$)
%and such that for every $i \in \{1,\ldots,k\}$ 
%the marking $m_{i}$ contains at least one token 
%in one of the given places.
Thus since this problem is decidable (Theorem \ref{th:infiniteVisit}) it follows that \LG is decidable in \evols{3}.

